perm filename BOOK.DOC[LSP,JRA] blob
sn#258219 filedate 1977-01-13 generic text, type T, neo UTF8
CONTENTS i
␈⊃
␈⊃
␈⊃ T A B L E O F C O N T E N T S
␈⊃
␈⊃
␈⊃
␈⊃CHAPTER PAGE
␈⊃
␈⊃ .1 Review and Reflection . . . . . . . . . 1
␈⊃
␈⊃
␈⊃ BIBLIOGRAPHY 28
␈⊃
␈⊃
␈⊃
␈⊃ INDEX 31
␈⊃ .1 Review and Reflection 1
␈⊃
␈⊃
␈⊃ .1 Review and Reflection
␈⊃
␈⊃
␈⊃ "I think that it is important to maintain a view
␈⊃ of the field that helps minimize the distance
␈⊃ between theoretical and practical work."
␈⊃
␈⊃ Saul Amarel, [Ama 72]
␈⊃
␈⊃By way of review we sketch the basic LISP evaluator of Section :
␈⊃eval plus the additional artifacts for label and function.
␈⊃
␈⊃There are two arguments to eval: a form 1, that is, an expression
␈⊃which can be evaluated; and an association list or symbol table. If
␈⊃the form is a constant, return that form. If the form is a variable,
␈⊃find the value of the variable in the current environment. If the
␈⊃form is a conditional expression, then evaluate it according to the
␈⊃semantics of conditional expressions.
␈⊃
␈⊃The form might also be a functional argument. In this case evaluation
␈⊃consists of associating the current environment with the function and
␈⊃returning that construct as value; in LISP this is done with the
␈⊃funarg device. Any other form seen by eval is assumed to be an
␈⊃application, that is, a function followed by arguments. The
␈⊃arguments are evaluated from left-to-right and the function is then
␈⊃applied to these arguments.
␈⊃
␈⊃The part of the evaluator which handles function application is
␈⊃called apply. apply takes three arguments: a LISP function, a list
␈⊃of evaluated arguments, and the current symbol table. If the function
␈⊃is one of the five LISP primitives then the appropriate action is
␈⊃carried out. If the function is a λ-expression then bind the formal
␈⊃parameters (the λ-variables) to the evaluated arguments and evaluate
␈⊃the body of the function. The function might also be the result of a
␈⊃functional argument binding; in this case apply the function to the
␈⊃arguments and use the saved environment, rather than the current
␈⊃environment, to search for non-local bindings. If we are applying
␈⊃the label operator, recalling page , we build a funarg-triple and
␈⊃new environment such that the environment bound in the triple is the
␈⊃new environment. We then apply the function to the arguments in this
␈⊃new environment.
␈⊃
␈⊃If the function has a name we look up that name in the current
␈⊃environment. Currently we expect that value to be a λ-expression,
␈⊃
␈⊃________________
␈⊃ 1 Throughout this section we will say "form", "variable",
␈⊃"λ-expression", etc. rather than "a representation of a" ... "form",
␈⊃"variable", "λ-expression", etc. No confusion should result, but
␈⊃remember that we are speaking imprecisely.
␈⊃ 2 .1
␈⊃
␈⊃
␈⊃which is then applied. However, since function names are just
␈⊃variables, there is no reason that the value of a function name could
␈⊃not be a simple value, say an atom, and that value can be applied to
␈⊃the arguments. This process can continue recursively until a true
␈⊃function-object is uncovered. Examination of apply on page will
␈⊃show that apply[X; ((A B)) ; ((X . CAR) ... )] will be handled
␈⊃correctly. The natural extension of this idea is to allow a computed
␈⊃function. That is, if the function passed to apply is not recognized
␈⊃as one of the preceding cases, then evaluate the function-part until
␈⊃it is recognized. Thus we will allow such forms as:
␈⊃
␈⊃ ((CAR (QUOTE (CAR (A . B)))) (QUOTE (A . B)))
␈⊃The addition of computed functions modifies apply (page ) slightly
␈⊃
␈⊃apply <= λ[[fn;args;environ] [iscar[fn] → car[arg1[args]];
␈⊃ iscons[fn] → cons[arg1[args];arg2[args]];
␈⊃ ... ...
␈⊃ islambda[fn] → eval[ body[fn];
␈⊃ pairlis[vars[fn];args;enviro
␈⊃ t → apply[ eval[fn;environ];
␈⊃ args;
␈⊃ environ] ]]
␈⊃
␈⊃The subset of LISP which is captured by this evaluator is a stong and
␈⊃useful language even though it lacks several of the more common
␈⊃programming language features 2. This subset is called the
␈⊃applicative subset of LISP, since its computational ability is based
␈⊃on the mathematical idea of function applications. We have
␈⊃persistently referred to our LISP procedures as LISP functions, even
␈⊃though we have seen some differences between the concept of function
␈⊃in mathematics and the concepts of procedure in LISP. It is the
␈⊃mathematical idea of function which the procedures of an applicative
␈⊃language are trying to capture. Regardless of differences in syntax
␈⊃and evaluation schemes, the dominant characteristic of an applicative
␈⊃language is that a given "function" applied to a given set of
␈⊃
␈⊃________________
␈⊃ 2 It is "strong", both practically and theoretically. It is
␈⊃sufficiently powerful to be "universal" in the sense that all
␈⊃computable functions are representable in LISP. In fact the
␈⊃eval-apply pair represents a "universal function", capable of
␈⊃simulating the behavior of any other computable function. The usual
␈⊃arguments about the halting problem ([Rog 67]) and related matters
␈⊃are easily expressed and proved in this LISP. Indeed, the original
␈⊃motivation for introducing the M-to-S expression mapping was to
␈⊃express the language constructs in the data domain. Only then was
␈⊃"S-expression LISP" used as the programming language. It was
␈⊃S. Russell who convinced Mc Carthy that the theoretical device
␈⊃represented in eval and apply could in fact be programmed on the
␈⊃IBM704.
␈⊃ .1 Review and Reflection 3
␈⊃
␈⊃
␈⊃arguments always produced the same result: either the computation
␈⊃produces an error, or it doesn't terminate, or it always produces a
␈⊃specific value. The applicative subset of LISP doesn't quite
␈⊃succeed. The treatement of free variables calls the environment into
␈⊃play. So in LISP, we must add a phrase about "a given environment",
␈⊃and the point becomes that the given computation in the given
␈⊃environment always has the same effect. That means we have no way to
␈⊃destructively change the environment. Languages which have such
␈⊃ability are said to have side-effects and are the business of the
␈⊃next chapter.
␈⊃
␈⊃LISP was the first language to exploit procedures as objects of the
␈⊃language. The idea has been generalized substantially in the
␈⊃intervening years. A concise statement of the more general principle
␈⊃appears in [Pop 68a].
␈⊃
␈⊃ "...This brings us to the
␈⊃ sbject of items. Anything
␈⊃ which can be the value of a
␈⊃ variable is an item. All
␈⊃ items have certain
␈⊃ fundamental rights.
␈⊃ 1. All items can be the actual parameters of f
␈⊃ 2. All items can be returned as results of fun
␈⊃ 3. All items can be the subject of assignment
␈⊃ 4.All items can be tested for equality.
␈⊃
␈⊃ ..."
␈⊃
␈⊃LISP performs well on the first two principles, allowing LISP
␈⊃functions to be the arguments as well as the results of functions.
␈⊃The fourth principle is more difficult; that is, test for the
␈⊃equality of two LISP functions. In can be shown ([Rog 67]) that no
␈⊃algorithm can be constructed which will perform such test. However
␈⊃in more selective settings, program equality can be established, both
␈⊃theoretically ([Man 74]), and practically ([Boy 75], [Dar 73],
␈⊃[Car 76]).
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃________________
␈⊃ 3 This issue will be postponed until Chapter .
␈⊃ 4 .1
␈⊃
␈⊃
␈⊃
␈⊃The language, POP-2, has also generalized the notion of function
␈⊃application in a slight, but significant, way. The generalization is
␈⊃called partial application. Given a function
␈⊃
␈⊃ f <= λ[[x1; ... ;xn] x]
␈⊃
␈⊃we compute a new function of n-m arguments by applying f to m
␈⊃arguments:
␈⊃
␈⊃ f[t1; ...; tm] <= λ[[x1; ...xn-m] x']
␈⊃
␈⊃
␈⊃where x' results form x by binding xn-(m+1) through xn to t1 through
␈⊃tm respectively.
␈⊃
␈⊃Further generalizations of partial application are imaginable
␈⊃([Sta 74]).
␈⊃
␈⊃We have pointed out several "procedural" differences. Our treatment
␈⊃of conditional expressions differs from the usual treatment of
␈⊃function application: our standard rule for function application is
␈⊃"call by value" which requires the evaluation of all arguments before
␈⊃calling the LISP function, whereas only some of the arguments to a
␈⊃conditional expression are evaluated. Note that the whole question of
␈⊃"evaluation of arguments" is a procedural one; arguments to functions
␈⊃aren't "evaluated" or "not evaluated", they just "are".
␈⊃
␈⊃We have seen different algorithms computing the same function; for
␈⊃example fact and fact1 (page ) both compute the factorial
␈⊃function. If there are different algorithms for computing factorial,
␈⊃then there are different alorithms for computing the value of an
␈⊃expression, and eval is just one such algorithm. Just as the essence
␈⊃of fact and fact1 is the factorial function, we should capture the
␈⊃essence expressed in eval. Put another way, when applications
␈⊃programmers use sqrt or p they have a specific mathematical function
␈⊃or constant in mind. The implementation of the language supplies
␈⊃approximations to these mathematical entities, and assuming the
␈⊃computations stay within the numerical ranges of the machine, the
␈⊃programmers are free to interpret any output as that which the
␈⊃mathematical entities would produce. More importantly the programmers
␈⊃have placed specific interpretations or meanings on symbols. We are
␈⊃interested in doing the same thing only we wish to produce a freer
␈⊃interpretation, which only mirrors the essential ingredients of the
␈⊃language constructs. That is, sqrt represents a function and p
␈⊃represents a constant. The eval-apply pair gives one interpretation
␈⊃to the meaning of functions and constants, but there are different
␈⊃interpretations and there are different eval-apply pairs.
␈⊃ .1 Review and Reflection 5
␈⊃
␈⊃
␈⊃The remainder of this section will resolve some of the tension
␈⊃between function and procedure. We will study some of the
␈⊃mathematical implications of applicative languages. First this will
␈⊃be done using the λ-calculus, a formal language for studying the
␈⊃concept of function. Then the results of this study will be applied
␈⊃to the applicative LISP subset.
␈⊃
␈⊃What does this discussion have to do with programming languages?
␈⊃Clearly the order of evaluation or reduction is directly applicable.
␈⊃Our study will also give insights into the problem of language
␈⊃specification. Do we say that the language specification consists of
␈⊃a syntactic component and some description of the evaluation of
␈⊃constructs in that language? Or do we say that these two components,
␈⊃syntax and a machine, are merely devices for describing or
␈⊃formalizing notions about some abstract domain of discourse? A
␈⊃related question for programmers and language designers involves the
␈⊃ideas of correctness and equivalence of programs. How do we know when
␈⊃a program is correct? This requires some notion of a standard
␈⊃against which to test our implementations 4. If our algorithms really
␈⊃are reflections of functional properties, then we should develop
␈⊃methods for verifying that those properties are expressed in our
␈⊃algorithms. Against this we must balance the realization that many
␈⊃programs don't fit neatly into this mathematical framework. Many
␈⊃programs are best characterized as themselves. In this case we should
␈⊃then be interested in verfying equivalence of programs. If we develop
␈⊃a new algorithm we have some responsibility to demonstrate that the
␈⊃algorithms are equivalent in very well defined ways 5.
␈⊃
␈⊃The study of formal systems in mathematical logic offers insight.
␈⊃There, we are presented with a syntax and a system of axioms and
␈⊃rules of inference. Most usually we are also offered a "model
␈⊃theory" which gives us interpretations or models for the syntactic
␈⊃formal system; the model theory usually supplies additional means of
␈⊃giving convincing arguments for the validity of statements in the
␈⊃formal system. The arguments made within the formal system are
␈⊃couched in terms of "provability" whereas arguments of the model
␈⊃theory are given in terms of "truth". For a discussion of formal
␈⊃systems and model theory see [Men 64].
␈⊃
␈⊃
␈⊃
␈⊃________________
␈⊃ 4 "Unless there is a prior mathematical definition of a language at
␈⊃hand, who is to say whether a proposed implementation is
␈⊃correct?" [Sco 72].
␈⊃
␈⊃ 5 Current theory is inadequate for dealing with many real
␈⊃programming tasks. However the realization that one has a
␈⊃responsibility to consider the questions, even informally, is a
␈⊃sobering one which more programmers should experience.
␈⊃ 6 .1
␈⊃
␈⊃
␈⊃
␈⊃C. W. Morris ([Mor 55]) isolated three perspectives on language,
␈⊃syntax, pragmatics, and semantics.
␈⊃
␈⊃Syntax: The synthesis and analysis of sentences in a language. This
␈⊃ area is well cultivated in programming language
␈⊃ specification.
␈⊃
␈⊃Pragmatics: The relation between the language and its user.
␈⊃ Evaluators, like tgmoaf, tgmoafr and eval, come under the
␈⊃ heading of pragmatics. Pragmatics are more commonly
␈⊃ referred to as operational semantics in discussions of
␈⊃ programming languages.
␈⊃
␈⊃Semantics: The relation between constructs of the language and the
␈⊃ abstract objects which they denote. This subdivision is
␈⊃ commonly referred to as denotational semantics.
␈⊃
␈⊃Put differently, syntax describes appearance, pragmatics describes
␈⊃implementation, and semantics describes meaning 6. Though there is a
␈⊃strong concensus on the syntactic tools for specifying languages 7,
␈⊃there is no concensus on adequate pragmatics and even less agreement
␈⊃on the adequancy of semantic descriptions. We will first outline the
␈⊃pragmatics questions and then discuss a bit more of the semantics
␈⊃issues. In this discussion we will use the language distinctions of
␈⊃Morris even though the practice is not commonly followed in the
␈⊃literature. Typically, syntax is studied precisely and semantics is
␈⊃"everything else"; however the distinction between computation
␈⊃(pragmatics) and truth (semantics) is important and should not be
␈⊃muddled.
␈⊃
␈⊃One thought is to describe the pragmatics of a language in terms of
␈⊃the process of compilation. That is, the pragmatics is specified by
␈⊃some canonical compiler producing code for some well-defined simple
␈⊃machine. The meaning of a program is the outcome of an interpreter
␈⊃interpreting this code. But then, to understand the meaning of a
␈⊃particular construct, this proposal requires that you read the
␈⊃
␈⊃________________
␈⊃ 6 This division of language reflects an interesting parallel between
␈⊃mathematical logic and programming languages: in mathematical logic
␈⊃we have deduction, computation, and truth; in programming language
␈⊃specification we have three analogous schools of thought: axiomatic,
␈⊃operational, and denotational. We won't go into details here, but see
␈⊃[Men 64] for the mathematical logic and [Dav 76] for a study of the
␈⊃interrelationships; see [Hoa 69] for a discussion of the axiomatic
␈⊃school; we will say more about the operational and denotational
␈⊃schools in this section.
␈⊃
␈⊃ 7 But see [Pra 73] for a contrary position.
␈⊃ .1 Review and Reflection 7
␈⊃
␈⊃
␈⊃description of a compiler and understand the simple machine. Two
␈⊃problems arise immediately. Compilers are not particularly
␈⊃transparent programs. Second, a very simple machine may not
␈⊃adequately reflect the actual mechanisms used in an implementation.
␈⊃This aspect is important if the semantic description is to be
␈⊃meaningful to an implementor.
␈⊃
␈⊃There is a more fundamental difficulty here if we consider the
␈⊃practical aspects of this proposal. When asked to understand a
␈⊃program written in a high-level language you think about the behavior
␈⊃of that program in a very direct way. The pragmatics is close to the
␈⊃semantics. You think about the computational behavior as it
␈⊃executes; you do not think about the code that gets generated and
␈⊃then think about the execution of that code.
␈⊃
␈⊃A more natural pragmatics for the constructs is given in terms of the
␈⊃run-time behavior of these constructs. The eval function describes
␈⊃the execution sequence of a representation of an arbitrary LISP
␈⊃expression. Thus eval is the semantic description of LISP. Such
␈⊃descriptions have a flavor of circularity which some find
␈⊃displeasing. However some circularity is inevitable; we must assume
␈⊃that something is known and does not require further explication. If
␈⊃you decide to describe the semantics of language L1 in a simpler
␈⊃language L2 then either L2 is "self evident" or you must give a
␈⊃description of the meaning of L2.
␈⊃
␈⊃So, realistically, the choice is where to stop, not whether to stop.
␈⊃The LISP position is that the language and data structures are
␈⊃sufficiently simple that self-description is satisfactory. Attempts
␈⊃have been made to give non-circular interpreter-based descriptions of
␈⊃semantics for languages other than LISP. There is a VDL description
␈⊃of PL/1, and a description of ALGOL 68 by a Markov algorithm. Both
␈⊃these attempts result in a description which is long and unmanageable
␈⊃for all but the most persistent.
␈⊃
␈⊃There are some compelling reasons for deciding on direct circularity.
␈⊃First, you need only learn one language. If the specification is
␈⊃given the source language, then you learn the programming language
␈⊃and the specification language at the same time. Second, since the
␈⊃evaluator is written in the language, we can understand the language
␈⊃by understanding the workings of the single program, eval; and if we
␈⊃wish to modify the pragmatics, we need change only one collection of
␈⊃high-level programs. If we wished to add new language constructs to
␈⊃LISP we need only modify eval so that it recognizes an occurrence of
␈⊃that new construct, and add a function to describe the interpretation
␈⊃of the construct. That modification might be extensive, but it will
␈⊃be a controlled revision rather than a complete reprogramming effort.
␈⊃
␈⊃We should mention that there is another common method for specifying
␈⊃ 8 .1
␈⊃
␈⊃
␈⊃the pragmatics of a programming language. The original Algol report
␈⊃([Alg 63]) introduced a standard for syntax specification: the BNF
␈⊃equation. It also gave a reasonably precise description of the
␈⊃pragmatics of Algol statements in natural language. The style of
␈⊃presentation was concise and clear, but suffers for the imprecision
␈⊃of natural language. Regardless, this style of description is quite
␈⊃common and is very useful. A recent report ([Moor 75a]) on the
␈⊃pragmatics of InterLISP used this descriptive style. If the language
␈⊃is quite complex, then a formal description can be equally complex.
␈⊃In Section we will see that our interpreter definition will
␈⊃extend nicely to richer subsets of LISP.
␈⊃
␈⊃A language description should not attempt to explain everything about
␈⊃a language. It need only explain what needs explaining. You must
␈⊃assume that your reader understands something ... . McCarthy:
␈⊃`Nothing can be explained to a stone' [McC 66]. A description of a
␈⊃language must be natural and must match the expressive power of the
␈⊃language. That is, it should model how the constructs are to be
␈⊃implemented. What is needed is a description which exploits, rather
␈⊃than ignores, the structure of the language. Mathematical notation
␈⊃is no substitute for clear thought, but we believe careful
␈⊃formulations of semantics will lead to additional insights in the
␈⊃pragmatics of language design 8. The task requires new mathematical
␈⊃tools to model the language constructs, and requires increased care
␈⊃on the part of the language designer.
␈⊃
␈⊃Let's look at the issue of syntax for a moment. A satisfactory
␈⊃description of much of programming language syntax is standard BNF.
␈⊃The BNF is a generative, or synthetic grammar. That is, the
␈⊃rewriting rules specifying how to generate well formed strings. An
␈⊃evaluator, on the other hand, takes a program representation as input
␈⊃and gives as output a representation of the value of executing the
␈⊃program. This implies that our evaluator is analytic rather than
␈⊃synthetic; it must have some way of analyzing the structure of the
␈⊃program.
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃________________
␈⊃ 8 R. D. Tennent has invoked this approach in the design of
␈⊃QUEST ([Ten 76]).
␈⊃ .1 Review and Reflection 9
␈⊃
␈⊃
␈⊃
␈⊃In [McC 62], John McCarthy introduced the concept of abstract
␈⊃analytic syntax. The idea is directly derivable from the LISP
␈⊃experience. The syntax is analytic, rather than synthetic, in the
␈⊃sense that it tells how to take programs apart -- how to recognize
␈⊃and select subparts of programs using predicates and selector
␈⊃functions 9. It is abstract in the sense that it makes no commitment
␈⊃to the external representation of the constitutents of the program.
␈⊃We need only be able to recognize the occurrence of a desired
␈⊃construct. For example:
␈⊃
␈⊃isterm <= λ[[t] or[ isvar[t];
␈⊃ isconst[t];
␈⊃ and[issum[t];isterm[addend[t]];isterm[augend[t]]]]]
␈⊃
␈⊃and the BNF equation:
␈⊃
␈⊃ <term> ::= <var> | <const> | <term> + <term>.
␈⊃
␈⊃issum, addend, and augend, don't really care whether the sum is
␈⊃represented as x+y, or +[x;y] or (PLUS X Y) or xy+. The different
␈⊃external representations are reflections of different concrete
␈⊃syntaxes; the above BNF equations give one. It is parsing which
␈⊃links a concrete syntax with the abstract syntax.
␈⊃
␈⊃Since the evaluator must operate on some internal representation of
␈⊃the source program, a representation reflecting the structure of the
␈⊃program (commonly known as a parse tree) is most natural. We can
␈⊃describe the evaluation of a program in terms of a function which
␈⊃operates on a parse tree using the predicates and selectors of the
␈⊃analytic syntax. Abstract syntax concerns itself only with those
␈⊃properties of a program which are of interest to an evaluator.
␈⊃
␈⊃The Meta expression LISP constitutes a concrete syntax. The
␈⊃M-to-S-expression translator is the parser which maps the external
␈⊃representation onto a parse (or computational) tree. The selectors
␈⊃and predicates of the analytic syntax are straightforward. Recall the
␈⊃BNF for LISP:
␈⊃
␈⊃<form> ::= <constant>
␈⊃ ::= <variable>
␈⊃ ::=<function>[<arg>; ... ;<arg>]
␈⊃ ::= [<form> → <form>; ... ;<form> → <form>]
␈⊃ ....
␈⊃
␈⊃
␈⊃________________
␈⊃
␈⊃ 9 We will deal with abstract synthetic syntax when we discuss
␈⊃compilers.
␈⊃ 10 .1
␈⊃
␈⊃
␈⊃Our evaluator needs to recognize constants (isconst), variables
␈⊃(isvar), conditional expressions (iscond), and applications
␈⊃(isfun+args). We need to write a function in some language
␈⊃expressing the values of these constructs. Since the proposed
␈⊃evaluator is to manipulate parse trees, and since the domain of LISP
␈⊃functions is binary trees, it should seem natural to use LISP itself.
␈⊃If this is the case, then we must represent the parse tree as a LISP
␈⊃S-expr and represent the selectors and recognizers as LISP functions
␈⊃and predicates.
␈⊃Perhaps:
␈⊃
␈⊃isconst <= λ[[x] or[ numberp[x];
␈⊃ eq[x;NIL];
␈⊃ eq[x;T];
␈⊃ and[not[atom[x]];eq[first[x];QUOTE]
␈⊃
␈⊃isvar <= λ[[x] and[atom[x]; not[isconst[x]]]]
␈⊃
␈⊃iscond <= λ[[x] eq[first[x];COND]]
␈⊃
␈⊃
␈⊃There are really two issues here: a representation of the analytic
␈⊃syntax of a language, and a representation in terms of the language
␈⊃itself. In conjunction, these two ideas give a natural and very
␈⊃powerful means of specifying languages.
␈⊃
␈⊃If this style of specification is really effective, then we should be
␈⊃able to specify other languages in a similar fashion. What are the
␈⊃weak points of LISP as a `real' programming language? Mainly the
␈⊃insistence on binary tree representations of data. Many applications
␈⊃could profit from other data representations. What we would then
␈⊃like is a language which has richer data structures than LISP but
␈⊃which is designed to allow LISP-style semantic specification. That
␈⊃is, we would be able to give an analytic syntactic specification for
␈⊃the language. We would be able to write an evaluator, albeit more
␈⊃complex than eval, in the language itself. The evaluator would
␈⊃operate on a representation of the program as a data structure of the
␈⊃language, just as eval operates on the S-expr translation of the LISP
␈⊃program. The concrete syntax would be specified as a set of BNF
␈⊃equations, and our parser would translate legal strings -- programs--
␈⊃into parse trees.
␈⊃In outline, to specify a construct we must have at least the follow
␈⊃
␈⊃ 1. A concrete production.
␈⊃ 2. An abstract data type.
␈⊃ 3. A mapping from 1 to 2.
␈⊃ 4. An evaluator for the abstract type.
␈⊃ .1 Review and Reflection 11
␈⊃
␈⊃
␈⊃In Chapter we will sketch a recent LISP-like language, EL1, which
␈⊃does follow these rules 10.
␈⊃
␈⊃From a discussion of syntax we have gravitated back to evaluation.
␈⊃After we reduce the questions of syntax of programming languages to
␈⊃questions of abstract systax and strip away many of the irrelevant
␈⊃syntactic differences, how many real differences between languages
␈⊃are there? Semantics addresses this issue.
␈⊃
␈⊃Many of the semantic ideas in applicative programming languages can
␈⊃be captured in λ-calculus ([Chu 41]). The λ-calculus was developed to
␈⊃supply a formalism for discussing the notions of function and
␈⊃function application. Rather than develop the syntax of λ-calculus,
␈⊃we will use the syntax of LISP; we will show how we can abstract from
␈⊃the discussion of LISP function, or procedure, to a discussion of
␈⊃mathematical function.
␈⊃
␈⊃LISP has borrowed heavily, but informally, from mathematics and
␈⊃logic. It uses the language of functions and functional composition,
␈⊃but the usual interpretation of LISP expressions is procedural. We
␈⊃want to relate that procedural knowledge to the formalism which we
␈⊃have been developing.
␈⊃
␈⊃Most of the description of LISP which we have given so far is
␈⊃classified as operational. That means our informal description of
␈⊃LISP and our later description of the LISP interpreter are couched in
␈⊃terms of "how does it work or operate". Indeed the purpose of eval
␈⊃was to describe explicitly what happens when a LISP expression is
␈⊃evaluated. We have seen (page ) that discussion of evaluation
␈⊃schemes is non-trivial; and that order of evaluation can effect the
␈⊃outcome (page ).
␈⊃
␈⊃However, many times the order of evaluation is immaterial 11. We saw
␈⊃on page that eval will perform without complaint when given a
␈⊃form f[ ... ] supplied with too many arguments. How much of eval is
␈⊃"really" LISP and how much is "really" implementation? On one hand
␈⊃we have said that the meaning of a LISP expression is by definition
␈⊃what eval will calculate using the representation of the expression.
␈⊃On the other hand, we claim that eval is simply an implementation.
␈⊃There are certainly other implementations; i.e, other LISP functions
␈⊃evali which have the same input-output behavior as our eval. The
␈⊃position here is not that eval is wrong in giving values to things
␈⊃like cons[A;B;C], but rather: just what is it that eval implements?
␈⊃
␈⊃
␈⊃________________
␈⊃ 10 Compare steps 1 through 4 with those on page .
␈⊃
␈⊃ 11 "One difficulty with the operational approach is that it
␈⊃(frequently) specifies too much": C. Wadsworth.
␈⊃ 12 .1
␈⊃
␈⊃
␈⊃This other way of looking at meaning in programming languages is
␈⊃exemplified by denotational or mathematical semantics. This
␈⊃perspective springs from a common mathematical, philosophical, or
␈⊃logical device of distinguishing between a representation for an
␈⊃object, and the object itself. The most usual guise is the
␈⊃numeral-number distinction. Numerals are notations (syntax) for
␈⊃talking about numbers (semantics). thus the Arabic numerals 2, 02,
␈⊃the Roman numeral II, and the Binary notation 10, all denote or
␈⊃represent the number two. In LISP, (A B), (A . (B)), (A , B) and
␈⊃(A . (B . NIL)) all are notations for the same S-expr. We want to
␈⊃say that a LISP form car[(A . B)] denotes A, or car[A] denotes
␈⊃undefined just as we say in mathematics that 2+2 denotes 4 or 1/0 is
␈⊃undefined.
␈⊃
␈⊃Similarly, we will say that the denotational counterpart of a LISP
␈⊃function is a mathematical function defined over an appropirate
␈⊃abstract domain. Before proceeding, we introduce some conventions to
␈⊃distinguish notation from denotation.
␈⊃
␈⊃We will continue to use italics:
␈⊃
␈⊃ A, B, ..., x, ... car, ...(A . B)
␈⊃
␈⊃as notation in LISP expressions. Gothic bold-face:
␈⊃
␈⊃ A, B, ..., x, ...car, ...(A . B)
␈⊃
␈⊃will represent denotations.
␈⊃
␈⊃Thus A is notation for A; car[cdr[(A B)]] denotes B; the mapping, car
␈⊃is the denotation of the LISP function car.
␈⊃
␈⊃Several areas of LISP must be subjected to an abstraction process.
␈⊃
␈⊃In particular, the operations involved in the evaluation process must
␈⊃be abstracted away. These involve an abstraction from LISP's call by
␈⊃value evaluation and its left to right order of evaluation of
␈⊃arguments. For example, the operation of composition of LISP
␈⊃functions is to denote mathematical composition; in LISP,
␈⊃car[cdr[(A B)]] means apply the procedure cdr to the argument (A B)
␈⊃getting (B); apply the procedure car to (B) getting B. Mathematically
␈⊃speaking, we have a mapping, carocdr which is a composition of the
␈⊃car and cdr mappings; the ordered pair <(A B) , B> is in the graph of
␈⊃this composed mapping. At this level of abstraction, any LISP
␈⊃characterization of a function is equally good; the "efficiency"
␈⊃question has been abstracted away. Many important properties of real
␈⊃programs can be discussed in this mathematical context; in
␈⊃particular, questions of equivalence and correctness of programs are
␈⊃more approachable.
␈⊃ .1 Review and Reflection 13
␈⊃
␈⊃
␈⊃As we remove the operational aspects, we discover a few critical
␈⊃properties of functions which must be reconcilled with LISP's
␈⊃procedures. We must treat the ideas of binding of variables, and we
␈⊃must handle the notion of function application.
␈⊃
␈⊃We already know that there are at least two binding strategies
␈⊃available: static binding and dynamic binding. The choice of strategy
␈⊃can effect the resultant computation. This computational difference
␈⊃must be studied. Similarly, we have discussed two calling styles:
␈⊃call-by-value and call-by-name; these computational devices must have
␈⊃interpretations in mathematics. To illuminate the problem we take an
␈⊃example in LISP.
␈⊃
␈⊃Consider:
␈⊃ λ[[z]
␈⊃ λ[[u]
␈⊃ λ[[z] u[B]][C]]
␈⊃ [λ[[x] cons[x;z]]] ]
␈⊃ [A]
␈⊃
␈⊃
␈⊃The dynamic binding strategy of LISP will bind z to A; then bind u to
␈⊃the functional argument, λ[[x] cons[x;z]]; next, z is rebound to C,
␈⊃and finally u[B] is evaluated. That involves binding x to B and
␈⊃evaluating cons[x;z]. Since we are using dynamic binding, the latest
␈⊃bindings of the variables are used. The latest bindings for x and z
␈⊃are B and C respectively, and the final value is therefore (B . C).
␈⊃
␈⊃We can obtain static binding by replacing λ[[x] cons[x;z]] by
␈⊃function[λ[[x] cons[x;z]]]. This has the effect of associating the
␈⊃varaible z with the atom A. As we know, the final result of the
␈⊃computation will be (B . A).
␈⊃
␈⊃Which scheme more adequately reflects our intuitions about properties
␈⊃of function? The dynamic binding scheme implements the notion of
␈⊃procedure application f[t] being the substitution of a copy of the
␈⊃body f with every occurrence of a formal parameter replaced with t.
␈⊃
␈⊃This substitution can be expressed as:
␈⊃
␈⊃subst <= λ[[x;y;z] [is_var[z] → [equal[y;z] → x; t → z];
␈⊃ is_app[z] → mk_app[ subst[x;y;func[z]]
␈⊃ subst[x;y;arglist[z]]];
␈⊃ eq[y;λ_var[z]] → z;
␈⊃ t → mk_λ[ λ_var[z];
␈⊃ subst[x;y;body[z]]]]]
␈⊃
␈⊃However, some implications of dynamic binding are in conflict with
␈⊃other properties we expect functions to possess. For example, we
␈⊃ 14 .1
␈⊃
␈⊃
␈⊃expect that a systematic remaining of formal parameters should not
␈⊃effect the definition of a function.
␈⊃
␈⊃ λ[[y] x] should denote the same function as λ[[w] x].
␈⊃
␈⊃But
␈⊃
␈⊃ λ[[x] λ[[y] x]][w] is not the same as λ[[x] λ[[w] x]][w]
␈⊃
␈⊃Using dynamic binding, the first results in λ[[y] w], the second
␈⊃gives λ[[w] w].
␈⊃
␈⊃If we wish to ban such anomalies, we need to be more careful in
␈⊃performing our substitutions. Closer examination of the last example
␈⊃shows that the result λ[[w] w] occurred because the substitution
␈⊃changed a non-local name (x) into a local name (w). The expect
␈⊃result would have been obtained if we had recognized the clash of
␈⊃names and replaced the formal parameter y with a new name, say u, and
␈⊃then performed the substitution, getting λ[[u] w] which is the same
␈⊃as λ[[y] w].
␈⊃
␈⊃Before giving a substitution rule which accounts for such changes of
␈⊃name we will relate this discussion with the notions of logic.
␈⊃
␈⊃A variable, x, is a free variable 12 in a <wfe>, x if:
␈⊃
␈⊃x is the variable, x.
␈⊃
␈⊃x is an application, f[A], and x is free in f or x is free in A.
␈⊃
␈⊃x is a λ-expression, λ[[y] M], and x is free in M and x is distinct
␈⊃ from y.
␈⊃
␈⊃Thus w is free in λ[[x] w].
␈⊃
␈⊃We can definea LISP predicate to test for free-ness:
␈⊃
␈⊃isfree <= λ[[x;z] [is_var[z] → [eq[x;z] → t; t → f]
␈⊃ is_app[z] → [isfree[x;func[z]] → t;
␈⊃ t → isfree[x;arglist[z]]];
␈⊃ eq[λ_var[z];x] → f;
␈⊃ t → isfree[x;body[z]]]]
␈⊃
␈⊃
␈⊃A variable is a bound variable in x if it occurs in x and is not free
␈⊃in x. For example, w is bound in λ[[w] w].
␈⊃
␈⊃
␈⊃________________
␈⊃ 12 Compare this definition of free with that in Section .
␈⊃ .1 Review and Reflection 15
␈⊃
␈⊃
␈⊃Using our new terminology, we can say that a substitution of actual
␈⊃parameter for formal parameter can be made provided no free variables
␈⊃of the actual parameter will become bound variables as a result of
␈⊃the substitution.
␈⊃
␈⊃Here is an appropriate substitution rule:
␈⊃
␈⊃subst' <= λ[[x;y;z] [is_var[z] → [eq[y;z] → x; t → z];
␈⊃ is_app[z] → mk_app[ subst'[x;y;func[z]];
␈⊃ subst'[x;y;arglist[z]]];
␈⊃ eq[y;λ_var[z]] → z;
␈⊃ not[isfree[y;body[z]]] → z;
␈⊃ not[isfree[λ_var[z];x]] → mk_λ[ x
␈⊃ λ_var[z];
␈⊃ subst[
␈⊃ y;
␈⊃ body[z]]];
␈⊃ t → λ[[u] mk_λ[ u;
␈⊃ subst'[ x;
␈⊃ y;
␈⊃ subst'[ u;
␈⊃ λ_var[z];
␈⊃ body[z]]]]]
␈⊃ [genvar[ ]] ]]
␈⊃
␈⊃where genvar is to supply a new identifier for use as a variable
␈⊃name.
␈⊃
␈⊃LISP does not use explicit substitution, but rather simulates the
␈⊃substitution using symbol tables. LISP embodies subst with the
␈⊃exception that the function construct simulates subst'. As we have
␈⊃seen, the use of subst can lead to unexpected results. The formal
␈⊃study of functionality which appears in the λ-calculus is based on
␈⊃subst'.
␈⊃
␈⊃The substitution rule, subst', is used to expressed the b-rule of the
␈⊃λ-calculus:
␈⊃
␈⊃(b): app ≡ subst'[arglist[app];λ_var[func[app]];body[func[app]]]
␈⊃
␈⊃where app is an anonymous λ-application, and ≡ designates a
␈⊃replacement rule which maintains the intended meaning of the
␈⊃expressions.
␈⊃ 16 .1
␈⊃
␈⊃
␈⊃
␈⊃There is another basic rule of the λ-calculus called the a-rule. The
␈⊃a-rule generalizes the notion that λ[[x] x] denotes the same function
␈⊃as λ[[w] x]; that is, subject to certain restrictions, we can change
␈⊃the formal parameter. The a-rule says:
␈⊃
␈⊃(a): fun ≡ λ[[u] mk_λ[u;subst'[u;λ_var[fun];body[fun]]][var]
␈⊃
␈⊃
␈⊃provided that not[isfree[var];body[fun]].
␈⊃
␈⊃To complete the descrption, axioms which govern the behavior of ≡
␈⊃must be given. Essentially ≡ acts as equality: it is an equivalence
␈⊃relation. The a and b-rules are called conversion rules; they
␈⊃express the essential behavior of functions and their applications.
␈⊃The a rule formalizes the notion that a function is unchanged if we
␈⊃change its formal parameters. This property is related to referential
␈⊃transparency. A language possesses referential transparency if the
␈⊃value of an expression which contains subexpressions depends only on
␈⊃the values of those subexpressions. For example, if the value of an
␈⊃expression changed because we changed the name of a variable in one
␈⊃of its subexpressions, then that would violate referential
␈⊃transparency. This means LISP is not a referentially transparent
␈⊃language; for a fixed environment, the value of λ[[x] cons[x;y]][A]
␈⊃is the same as λ[[z] cons[x;y]][A], but need not be the same as
␈⊃λ[[x] cons[x;z]][A]. The difficulty again is the treatment of free
␈⊃variables: dynamic binding violates referential transparency. The
␈⊃λ-calculus is statically bound and does possess referential
␈⊃transparency. Referential transparency is not simply a worthwhile
␈⊃theoretical property; its corollary, static binding, is a very useful
␈⊃practical property. In programming terms, referential transparency
␈⊃mens that to understand a particular progam we need only understand
␈⊃the effect of the subprograms rather than understand the
␈⊃implementation of those subprograms. This idea is closely related to
␈⊃the notion of modular programming. We will discuss some implications
␈⊃of static binding in Section 13.
␈⊃
␈⊃The b-rule expresses the intent of function application. We would
␈⊃then expect that a model of the λ-calculus would have a domain
␈⊃consisting of functions; and require that the b-rule be reflected in
␈⊃the model as function application. The equality preserving properties
␈⊃of the a and b rules would require that if f[a] = g[a] in the model,
␈⊃then any a or b manipulations of those expressions will not affect
␈⊃that equality.
␈⊃
␈⊃The discussion has centered around binding strategies. We should now
␈⊃
␈⊃________________
␈⊃ 13 There have been recent investigations ([Hew 76], [Sus 75]) of
␈⊃statically bound LISP-like languages.
␈⊃ .1 Review and Reflection 17
␈⊃
␈⊃
␈⊃discuss calling style. The conversion rules have no restrictions
␈⊃concerning an order of application. If the hypotheses for a rule is
␈⊃satisfied, then it may be applied. That is as it should be. In the
␈⊃reduction of a λ-expression there may be several reductions possible
␈⊃at any one time. If we design a λ-calculus machine, it might be
␈⊃specified with a preferred order. The machine reflects "procedure";
␈⊃the calculus reflects "function".
␈⊃
␈⊃An interpretation of the conversion rules as rules of compuatation
␈⊃requires the establishment of a notion of what is to be computed.
␈⊃The conversion rules simply state equivalences between expressions.
␈⊃When the b rule is applied in a manner analogous to LISP's λ-binding,
␈⊃that is, to replace an application with the appropriately substituted
␈⊃body, then the b rule is called a reduction rule; and the application
␈⊃of the rule is called a reduction step. There are two common
␈⊃strategies for choosing a reduction step: applicative order and
␈⊃normal order.
␈⊃
␈⊃Applicative order corresponds to call-by-value, reducing the argument
␈⊃before reducing the function. Normal order reduces the function
␈⊃application first; this corresponds to call-by-name. As we know from
␈⊃LISP, the order of evaluation can influence the termination of a
␈⊃computation. That observation holds for the λ-calculus. To understand
␈⊃what corresponds to termination in the formalism, requires a bit more
␈⊃terminology. We will say that a λ-expression is in normal form if it
␈⊃contains no expression reducible by the β rule. Not all expressions
␈⊃have normal forms: let D name λ[[x] x[x]]; then D[D] does not have a
␈⊃normal form. Every b transformation of D produces a new expression
␈⊃which is also b reducible. Not all reduction sequences yield a
␈⊃normal form: when λ[[x] y][D] is reduced in normal order, a normal
␈⊃form results; whereas applicative order will not yield a normal form.
␈⊃
␈⊃The application of the reduction rules, in either applicative or
␈⊃normal order, can be considered a computation scheme. The process of
␈⊃reducing an expression is the computation, and a computation
␈⊃terminates if that reduction produces a normal form. With this
␈⊃interpretation, some computations terminate and some don't. A <wfe>
␈⊃has a normal form just in the case that a reduction sequence
␈⊃terminates. The computational interpretation of the λ-calculus rules
␈⊃can be extended to the development of λ-calculus machines ([Lan 64]).
␈⊃The λ-calculus machines can simulate the reduction rules in several
␈⊃ways; since the rules make no commitment for order of application,
␈⊃that choice is open. Also, the reduction rules are described in
␈⊃terms of substitutions; a machine might simulate this facet directly
␈⊃or might employ a mechanism like the LISP symbol table.
␈⊃
␈⊃This discussion suggests some interesting problems. First, there may
␈⊃well be two or more sequences of reductions for a λ-expression;
␈⊃assuming they terminate, is there any reason to believe that these
␈⊃ 18 .1
␈⊃
␈⊃
␈⊃reduction sequences will yield the same normal forms? Second, if we
␈⊃have two λ-expressions which reduce to distinct normal forms, is
␈⊃there any reason to believe that they are "inherently different"
␈⊃λ-expressions?
␈⊃
␈⊃The first question is easier to answer. If both reduction sequences
␈⊃terminate then they result in the same normal form. This is called
␈⊃the Church-Rosser theorem.
␈⊃
␈⊃The second question requires some explanation of "inherently
␈⊃different". At one level we might say that by definition,
␈⊃expressions with different normal forms are "inherently different".
␈⊃But thinking of λ-expressions as functions, to say two λ-expressions
␈⊃are "different" is to say we can exhibit arguments such that the
␈⊃value of application of one function is not equal to the value of the
␈⊃other function application 14. C. Boehm has established this for
␈⊃λ-expressions which have normal forms.
␈⊃
␈⊃However the situation changes when we examine λ-expressions which do
␈⊃not have normal forms. Recalling the intuitive relationship between
␈⊃non-termination and "no normal form", we might expect that all
␈⊃expressions without normal form are "equivalent". However, it can be
␈⊃shown that such an identification would lead to contradictions. We
␈⊃might also expect that λ expressions without normal forms are
␈⊃"different" from expressions which do have normal forms. This is
␈⊃also not true; [Wad 71] exhibits two expressions, I and J with and
␈⊃without normal form, respectively. However these two expressions are
␈⊃the "same" in the sense that 3 and 2.99999 ... are the "same". That
␈⊃is, J is the limit of a sequence of approximations to I. Also, we
␈⊃can exhibit two λ-expressions, Y1 and Y2, both without normal form,
␈⊃which are distinct in that no reduction sequence will reduce one to
␈⊃the other; but our intuition says that they are "the same function"
␈⊃in the sense that, for any argument, a we supply, both reductions
␈⊃result in the same expression. That is Y1[a] = Y2[a] 15.
␈⊃
␈⊃The reduction rules of the λ-calculus cannot help us. The resolution
␈⊃of the idea of "same-ness" requires stronger analysis 16. We can
␈⊃give an interpretation to the λ-calculus such that in that
␈⊃interpretation the pairs I and J, or Y1 and Y2, have the same
␈⊃
␈⊃________________
␈⊃ 14 If two functions satisfy this then they are said to be
␈⊃extensionally equal.
␈⊃
␈⊃ 15 Note that f[a] may have a normal form even though f does not.
␈⊃
␈⊃ 16 The interpretation of "same-ness" which we have been using is
␈⊃that of extensional equality. That is, two functions are considered
␈⊃the same function if no differences can be detected under application
␈⊃of the functions to any arguments.
␈⊃ .1 Review and Reflection 19
␈⊃
␈⊃
␈⊃meaning. This should be a convincing argument for maintaining that
␈⊃they are the "same function" even though the reduction rules are not
␈⊃sufficient to display that equivalence 17. D. Scott has exhibited a
␈⊃model or interpretation of the λ-calculus, and D. Park has shown the
␈⊃equivalence in this model of Y1 and Y2, and C. Wadsworth as shown the
␈⊃equivalence of I and J.
␈⊃
␈⊃As we said at the beginning of the section, this calculus was
␈⊃intended to explicate the idea of "function" and "function
␈⊃application". There is a reasonably subtle distinction between
␈⊃Church's conception of a function as a rule of correspondence, and
␈⊃the usual set-theoretic view of a function as a set of ordered pairs.
␈⊃In the latter setting we rather naturally think of the elements of
␈⊃the domain and range of a function as existing prior to the
␈⊃construction of the function:
␈⊃
␈⊃ "Let f be the function {<x,1>, <y,2>, ...}".
␈⊃
␈⊃When we think of a function given as a predetermined set of ordered
␈⊃pairs we do not expect functions which can take themselves as
␈⊃arguments like f[f]. Such functions are called self-applicative.
␈⊃Several languages, including LISP, allow the procedural analog of
␈⊃self applicative functions. They are an instance of functional
␈⊃arguments (Section ). The LISP function discussed in the
␈⊃problem on page is an instance of a self-applicative LISP
␈⊃function. Since we can deal with self-application as a procedural
␈⊃concept at least, perhaps some of this understanding will help with
␈⊃the mathematical questions. Again, we turn to the λ-calculus.
␈⊃
␈⊃The calculus is an appropriate tool for studying self-application and
␈⊃function-values since syntax allows such constructs. Indeed
␈⊃everything in the calculus is a representation of a function. Compare
␈⊃this with the condition in LISP when we think of the S-expression
␈⊃representation of language as the language itself. Then the
␈⊃distinction between program and data disappears, just as it does in
␈⊃the λ-calculus. The conversion rules of the calculus allow a
␈⊃λ-expression to be applied to any λ-expression including the
␈⊃expression itself 18.
␈⊃
␈⊃A similar situation exists in the programming language LISP. We can
␈⊃evaluate expressions like:
␈⊃
␈⊃((LAMBDA (X) x) (LAMBDA (X) x))
␈⊃________________
␈⊃ 17 This demonstration also gives credence to the position that the
␈⊃meaning transcends the reduction rules. Compare the incompleteness
␈⊃results of K. Godel.
␈⊃
␈⊃ 18 There are logical difficulties, like Russell's paradox, which
␈⊃arise if we allow unrestricted self-application.
␈⊃ 20 .1
␈⊃
␈⊃
␈⊃As we move again from procedural notions to more denotational
␈⊃concepts we should remark that denotational interpretations have been
␈⊃introduced before. When we said (page ) that:
␈⊃ f[a1; ... an] = eval[(F A1 ... An)],
␈⊃
␈⊃we were relating a denotational notion with an operational notion.
␈⊃The left hand side of this equation is denotational; it expresses a
␈⊃functional relationship. The right hand side is operational,
␈⊃expressing a procedure call. This denotational-operational
␈⊃distinction is appropriate in a more general context. When we are
␈⊃presented with someone's program and asked "what does it compute?" we
␈⊃usually begin our investigation operationally, discovering "what does
␈⊃it do?" 19. Frequently, by tracing its execution, we can discover a
␈⊃denotational description: E.g., "ah! it computes the square root".
␈⊃
␈⊃When great mother was presented it was given as an operational
␈⊃exercise, with the primary intent of introducing the LISP evaluation
␈⊃process without involving complicated names and concepts. Forms
␈⊃involving great mother were evaluated perhaps without understanding
␈⊃the denotation, but if asked "what does great mother do?" you would
␈⊃be hard pressed to given a comprehensible purely operational
␈⊃definition. However, you might have discovered the intended nature of
␈⊃great mother yourself; then it would be relatively easy to describe
␈⊃its (her) behavior. Indeed, once the denotation of great mother has
␈⊃been discovered questions like "What is the value of
␈⊃tgmoaf[(CAR (QUOTE (A . B)))]? " are usually answered by using the
␈⊃denotation of tgmoaf: "what is the value of car[(A . B)]?" The
␈⊃question of how one gives a convincing argument that eval does
␈⊃faithfully represent LISP evaluation is the subject of [Gor 73].
␈⊃
␈⊃In discussing models for LISP, we will parallel our development of
␈⊃interpreters for LISP since each subset, tgmoaf, tgmoafr, and eval,
␈⊃will also introduce new problems for our mathematical semantics.
␈⊃
␈⊃Our first LISP subset considers functions, compostion, and constants.
␈⊃Constants will be elements of our domain of interpretation. Our
␈⊃domain will include the S-expressions since most LISP expressions
␈⊃denote S-exprs; since many of our LISP functions are partial
␈⊃functions, it is convenient to talk about the undefined value, B. We
␈⊃wish to extend our partial functions to be total functions on an
␈⊃extended domain. As before (page ), we shall call this extended
␈⊃domain S.
␈⊃
␈⊃Before we can talk very precisely about the properties of
␈⊃mathematical functions denoted by LISP functions, we must give more
␈⊃
␈⊃________________
␈⊃ 19 Another common manifestation of this "denotation" phenomonon is
␈⊃the common programmer complaint: "It's easier to write your own than
␈⊃to understand someone else's."
␈⊃ .1 Review and Reflection 21
␈⊃
␈⊃
␈⊃careful study to the nature of domains. Our primitive domain is
␈⊃<atom>. Its intuitive structure is quite simple, basically just a
␈⊃set of atoms or names with no inherent relationships among them.
␈⊃Another primitive domain is Tr, the domain of truth values.
␈⊃
␈⊃The domain <sexpr> is more complex; it is a set of elements, but many
␈⊃elements are related. In our discussion of <sexpr> on page we
␈⊃made it clear that there is more than syntax involved. We could say
␈⊃that for s1 and s2 in <sexpr> the essence of "dotted pair" is
␈⊃contained in the concept of the set-theoretic ordered pair, <s1,s2>.
␈⊃Thus the "meaning" of the set of dotted pairs is captured by
␈⊃Cartesian product, <sexpr> x <sexpr>.
␈⊃
␈⊃Let's continue the analysis of:
␈⊃ <sexpr> ::= <atom> | (<sexpr> . <sexpr>).
␈⊃
␈⊃We are trying to interpret this BNF equation as a definition of the
␈⊃domain <sexpr>. Reasonable interpretations of "::=" and "|" appear to
␈⊃be equality and set-theoretic union, respectively. This results in
␈⊃the equation:
␈⊃ <sexpr> = <atom> ∪ <sexpr> x <sexpr> .
␈⊃
␈⊃This looks like an algebraic equation, and as such, may or may not
␈⊃have solutions. This particular "domain equation" has a solution:
␈⊃the S-exprs.
␈⊃
␈⊃There is a natural mapping of BNF equations onto such "domain
␈⊃equations", and the solutions to the domain equations are sets
␈⊃satisfying the abstract essence of the BNF.
␈⊃
␈⊃The mapping process is also applicable to the language constructs.
␈⊃Consider the BNF equations for a simple applicative subset of LISP:
␈⊃ <form> ::= <variable> | λ[[<variable>] <form> | <variable [<form>]
␈⊃
␈⊃We would like to describe the denotations of these equations in a
␈⊃style similar to that used for <sexpr>'s. The denotations of the
␈⊃expressions, <form>, of applications, <variable>[form>], and of the
␈⊃variables, <variables>, are just constants of the language; call this
␈⊃domain C.
␈⊃
␈⊃Expressions of the form "λ[[<variable>] <form>]" are to denote
␈⊃functions. First we consider the set of functions from C to C. Write
␈⊃that set as C → C. Then our domain equation is expressed:
␈⊃
␈⊃ C = C→C ∪ C
␈⊃
␈⊃This equation has no interesting solutions. A simple counting
␈⊃argument will establish that unless the domain C is a single element,
␈⊃then the number of functions in C → C is greater than the number of
␈⊃ 22 .1
␈⊃
␈⊃
␈⊃elements in C. This does not say that there are no models of the
␈⊃λ-calculus. It says is that our interpretation of "→" is too broad.
␈⊃
␈⊃What is needed is an interpretation of functionality which will allow
␈⊃a solution to the above domain equation; it should allow a natural
␈⊃interpretation such that the properties which we expect functions to
␈⊃possess are true in the model. Scott gave one such interpretation of
␈⊃"→", defining the class of "continuous functions". This class of
␈⊃functions is restricted enough to satisfy the domain equation, but
␈⊃broad enough to act as the denotations of procedures in applicative
␈⊃programming languages. We will use the notation "[D1 → D2]" to mean
␈⊃"the set of continuous functions from domain D1 to domain D2". It is
␈⊃the continuous functions which first supplied a model for the
␈⊃λ-calculus and it is these functions which supply a basis for a
␈⊃mathematical model of LISP.
␈⊃
␈⊃We can assume that the LISP primitives denote specific continuous
␈⊃functions. For example, the mathematical counterpart to the LISP
␈⊃function car is the mapping car from S to S defined as follows:
␈⊃
␈⊃
␈⊃ car: [S → S]
␈⊃
␈⊃ is B if t is atomic
␈⊃ car(t) is t1 if t is (t1 . t2)
␈⊃ is B if t is B.
␈⊃
␈⊃
␈⊃Similar strategy suffices to give denotations for the other primitive
␈⊃LISP functions and predicates. For example:
␈⊃
␈⊃
␈⊃ atom: [S → S]
␈⊃
␈⊃ is f if t is not atomic.
␈⊃ atom(t) is t if t is atomic.
␈⊃ is B if t is B.
␈⊃
␈⊃
␈⊃Notice that these functions are strict: f(B) = B.
␈⊃
␈⊃Corresponding to tgmoaf, we will have a function, Dtg, which maps
␈⊃expressions onto their denotations. Since Dtg is another mapping
␈⊃like r, we will use the "(" and ")" brackets to enclose LISP
␈⊃constructs. We need to introduce some notation for elements of the
␈⊃sets <sexpr> and <form>. Let s range over <sexpr> and f range over
␈⊃<form>, then we can write:
␈⊃
␈⊃ Dtg(s) = s
␈⊃ Dtg(car[f]) = car(Dtg(f))
␈⊃ .1 Review and Reflection 23
␈⊃
␈⊃
␈⊃with similar entries for cdr, cons, eq, and atom. The structure of
␈⊃this definition is very similar to that of tgmoaf.
␈⊃
␈⊃Now we continue to the next subset of LISP, adding conditional
␈⊃expressions to our discussion. As we noted on page , a degree of
␈⊃care need be taken when we attempt to interpret conditional
␈⊃expressions in terms of mappings. We can simplify the problem
␈⊃slightly: it is easy to show that the conditional expression can be
␈⊃formulated in terms of the simple if-expression: if[p1;e1;e2]. We
␈⊃will display a denotation for such if expressions. It will be a
␈⊃mathematical function, and therefore the evaluation order will have
␈⊃been abstracted out 20.
␈⊃Let if denote if where:
␈⊃
␈⊃ if: [TrxSxS → S]
␈⊃
␈⊃ is y if x is t
␈⊃ if(x,y,z) is z, if x is f.
␈⊃ is B, otherwise
␈⊃
␈⊃This interpretation of conditional expressions is appropriate for
␈⊃LISP; other interpretations of conditionals are possible. For
␈⊃example:
␈⊃
␈⊃ if1: [TrxSxS → S]
␈⊃
␈⊃ is y if x is t
␈⊃ if1(x,y,z) is z, if x is f.
␈⊃ is B if x is B and y ≠ z
␈⊃ is y if x is B and y = z 21.
␈⊃
␈⊃Neither if nor if1 are strict mappings.
␈⊃
␈⊃To add if expressions to Dtg, yielding Dtgr we include:
␈⊃
␈⊃ Dtgr(if[f1 ; f2; f3]) = if(Dtgr(f1),Dtgr(f2),Dtgr(f3))
␈⊃
␈⊃The next consideration is the denotational description of LISP
␈⊃identifiers. Identifiers name either S-exprs or LISP functions.
␈⊃
␈⊃________________
␈⊃ 20 Recall the comment of Wadsworth (page 11). Indeed, the use of
␈⊃conditional expressions in the more abstract representations of LISP
␈⊃functions frequently is such that exactly one of the pi's is t and
␈⊃all the others are f. Thus in this setting, the order of evaluation
␈⊃of the predicates is useful for "efficiency" but not necessary to
␈⊃maintain the sense of the definition. See page .
␈⊃
␈⊃ 21 Basing conditional expressions on if1 would give [car[A] → 1;
␈⊃t → 1] value 1.
␈⊃ 24 .1
␈⊃
␈⊃
␈⊃Thus an identifier denotes either an object on our domain S or
␈⊃denotes a function object. Let Fn name the set of continuous
␈⊃functions: Sn=0[Sn → S], and Id be <identifier>∪B. We know that the
␈⊃value of a LISP <identifier> (page ) depends on the current
␈⊃environment. Then we might characterize the set of environments, env,
␈⊃as:
␈⊃
␈⊃ [Id → S ∪ Fn].
␈⊃
␈⊃That is, an element of env is a continuous function which maps an
␈⊃identifier either onto a S-expr or onto an n-ary function from
␈⊃S-exprs to S-exprs. This is the essence of the argument used in
␈⊃introducing assoc (Section ). Note that assoc[x;l] = l(x) is
␈⊃another instance of a operational-denotational relationship.
␈⊃
␈⊃Given a LISP identifier, x, and a member of env, say the function
␈⊃{<x,2>,<y,4>}, then the new D should map x onto 2. This is an
␈⊃intuitive way of saying that D should map a member of <identifier>
␈⊃onto a function. This function will map a member of env onto an
␈⊃element of S. Introducing i as a meta-variable to range over
␈⊃<indentifier>, then for l ε env we have:
␈⊃ D(i)(l) = l(i)
␈⊃
␈⊃The meaning or denotation of a identifier is a function; whereas the
␈⊃value of an identifier is an element of S∪Fn.
␈⊃
␈⊃The treatment of identifiers leads directly into the denotional
␈⊃aspects of function application. We shall maintain the parallels
␈⊃between evaluation and denotation, by giving De and Da corresponding
␈⊃to eval and apply. Let g be a member of <function> and f be a member
␈⊃of <form>, then for a given element of env, Da maps g onto an element
␈⊃of Fn, and De maps f onto an element of S.
␈⊃For example: Da(car)(l) = car
␈⊃
␈⊃Similar equations hold for the other LISP primitive functions and
␈⊃predicates. In general, then:
␈⊃
␈⊃ Da(f)(l) = l(f), where f ε <function>.
␈⊃
␈⊃To describe the evaluation of a function-call in LISP we must add an
␈⊃equation to De:
␈⊃
␈⊃ De(f[s1, ...,sn])(l) =
␈⊃Da(f)(l)(De(s1)(l), ...,De(sn)(l))
␈⊃
␈⊃We must also make consistent modifications to the previous clauses of
␈⊃Dtgr to account for environments. That is, the value of a constant
␈⊃is independent of the specific environment in which it is evaluated.
␈⊃ De(s)(l) = s.
␈⊃ .1 Review and Reflection 25
␈⊃
␈⊃
␈⊃We must also extend our equations to account for conditional
␈⊃expressions.
␈⊃
␈⊃Before we get very far in applying functions to values we must give a
␈⊃mathematical characterization of function definitions. In this
␈⊃section we will handle λ-notation without free variables, postponing
␈⊃more complex cases to Section .
␈⊃
␈⊃Assuming the only free variables in x are among the xi's, the
␈⊃denotation of λ[[x1; ...; xn] x] in a specified environment should be
␈⊃a function from Sn to S such that:
␈⊃
␈⊃ Da(λ[[v1; ... ;vn]s])(l) =
␈⊃λ(x1, ..., xn)De(s)(l : <x1,v1>, ..., <xn,vn>)
␈⊃
␈⊃where λ is the LISP λ-notation and λ is its mathematical counterpart
␈⊃and vi is the denotational counterpart of vi, and (l : ... ) means
␈⊃the environmeent l augmented with the explicitly given pairs.
␈⊃
␈⊃That is, (l : <x1,v1>, ..., <xn,vn>) is a modification of l such that
␈⊃each vi is bound to the corresponding xi.
␈⊃That is: (l : <x,v>) is: λ(v1) if v = B then B
␈⊃ else if v1 = B then B
␈⊃ else if v1 = x then v
␈⊃ else l(v1).
␈⊃
␈⊃where: if p then q else r is if(p,q,r).
␈⊃
␈⊃In more detail: λ(x1, ... ,xn)e(x1, ... ,xn) is a function f: Sn → S
␈⊃such that:
␈⊃
␈⊃ is e(t1, ... ,tn) if m≥n and ∀i ti ≠ B. 22
␈⊃f(t1, ..., tm)
␈⊃ is B otherwise
␈⊃
␈⊃
␈⊃Analysis of our study will show that one of the larger difficulties
␈⊃was caused by our insistence on dealing with type-free languages.
␈⊃Self-application is one indication of this. We can show that imposing
␈⊃a type structure on our language will also solve many of the
␈⊃questions of non-termination. In a typed λ-calculus an expression
␈⊃will always have a normal form ([Mor 68]). Computationally this means
␈⊃that all the programs will terminate. Also models for typed
␈⊃λ-calculus are much more readily attained. However the type free
␈⊃calculus is a stronger system, and requiring all expressions to have
␈⊃a consistent type structure rules out several useful constructs; in
␈⊃
␈⊃________________
␈⊃ 22 Note that this equation allows the LISP trick of supplying too
␈⊃many arguments.
␈⊃ 26 .1
␈⊃
␈⊃
␈⊃particular, the λ-calculus counterpart to the LISP label operator
␈⊃cannot be consistently typed.
␈⊃
␈⊃From the practical side, a typed structure is also a mixed blessing.
␈⊃LISP programmers frequently miss the declarations of common
␈⊃programming languages. Language delarations are a form of typing and
␈⊃can be quite helpful in pinpointing programming errors; declarations
␈⊃can also be used by compilers to help produce optimized code. However
␈⊃those same programmers want to subvert the type structure, typically
␈⊃in the name of efficiency or expediency. Also a type structure can
␈⊃be a real nuisance when trying to debug a program; it is frequently
␈⊃desireable to examine and modify the representations of abstract data
␈⊃structures. Those kinds of operations imply the ability to ignore the
␈⊃type information.
␈⊃
␈⊃Logically, the next addition to D would involve recursion and
␈⊃function definitions: label and "<=". We know that the LISP label
␈⊃operator is similar to "<=", but label builds a temporary definition,
␈⊃while "<=" modifies the environment. Programming language constructs
␈⊃which modify the environment are said to have side-effects and are an
␈⊃instance of what is called a imperative construct. Since our main
␈⊃interest lies in the programming aspects, we will pursue the
␈⊃procedural aspects and postpone the mathematics. The next chapter
␈⊃introduces the procedural aspects of imperative constructs and in
␈⊃Section we will investigate some of the mathematical aspects of
␈⊃"<=" and label.
␈⊃
␈⊃
␈⊃
␈⊃ Problems
␈⊃
␈⊃
␈⊃I. Recall the problem on page , dealing with the following
␈⊃factorial algorithm:
␈⊃
␈⊃ fact <= λ[[n] f[function[f]; n]]
␈⊃
␈⊃ f <= λ[[g;n][n=0 → 1; t → *[n; g[g; n-1]] ]]
␈⊃
␈⊃Rewrite f in terms a unary function t:
␈⊃
␈⊃ t <= λ[[x] function[λ[[n][n=0 → 1; t → *[n; x[n-1]] ]]]].
␈⊃
␈⊃Show that fact = t[fact].
␈⊃ .1 Review and Reflection 27
␈⊃
␈⊃
␈⊃
␈⊃II. The language described by the a and b rules doesn't look
␈⊃particularly rich, similar in power to LISP with just function
␈⊃application but without conditional expressions. That is only an
␈⊃illusion. Show that we can represent a simple if function
␈⊃if[p;then;otherwise]. Hint: show that λ[[x;y] y] is a good
␈⊃representation for f and λ[[x;y] x] is a good representation for t.
␈⊃ 28 BIBLIOGRPAHY 1.
␈⊃
␈⊃
␈⊃ BIBLIOGRAPHY
␈⊃
␈⊃
␈⊃
␈⊃
␈⊃The basic form of an entry consists of three items:
␈⊃
␈⊃ 1. A short name which is how the document is referenced in the
␈⊃ text.
␈⊃
␈⊃ 2. The full bibliographical reference.
␈⊃
␈⊃ 3. A sequence of pages in the text which refer to this document.
␈⊃ If the document is not referenced the statement [ norefs ]
␈⊃ appears instead.
␈⊃
␈⊃[Alg 63] 8 [ norefs ]
␈⊃
␈⊃[Ama 72] 1 [ norefs ]
␈⊃
␈⊃[Boy 75] 3 [ norefs ]
␈⊃
␈⊃[Car 76] 3 [ norefs ]
␈⊃
␈⊃[Chu 41] 11 [ norefs ]
␈⊃
␈⊃[Dar 73] 3 [ norefs ]
␈⊃
␈⊃[Dav 76] 6 [ norefs ]
␈⊃
␈⊃[Gor 73] 20 [ norefs ]
␈⊃
␈⊃[Hew 76] 16 [ norefs ]
␈⊃
␈⊃[Hoa 69] 6 [ norefs ]
␈⊃
␈⊃[Lan 64] 17 [ norefs ]
␈⊃
␈⊃[Man 74] 3 [ norefs ]
␈⊃
␈⊃[McC 62] 9 [ norefs ]
␈⊃
␈⊃[McC 66] 8 [ norefs ]
␈⊃
␈⊃[Men 64] 5 [ 6 ]
␈⊃
␈⊃[Moor 75a] 8 [ norefs ]
␈⊃
␈⊃[Mor 55] 6 [ norefs ]
␈⊃ 1. BIBLIOGRPAHY 29
␈⊃
␈⊃
␈⊃[Mor 68] 25 [ norefs ]
␈⊃
␈⊃[Pop 68a] 3 [ norefs ]
␈⊃
␈⊃[Pra 73] 6 [ norefs ]
␈⊃
␈⊃[Rog 67] 2 [ 3 ]
␈⊃
␈⊃[Sco 72] 5 [ norefs ]
␈⊃
␈⊃[Sta 74] 4 [ norefs ]
␈⊃
␈⊃[Sus 75] 16 [ norefs ]
␈⊃
␈⊃[Ten 76] 8 [ norefs ]
␈⊃
␈⊃[Wad 71] 18 [
␈⊃ INDEX 31
␈⊃
␈⊃
␈⊃a-rule 16
␈⊃b-rule 15
␈⊃analytic syntax 9
␈⊃bound variable 14
␈⊃computed function 2
␈⊃concrete syntax 9
␈⊃denotational 12
␈⊃free variable 14
␈⊃operational 11
␈⊃partial application 4
␈⊃reduction rule 17
␈⊃referential transparency 16
␈⊃self-applicative 19
␈⊃